perm filename ELEPHA.AX[S81,JMC] blob sn#581743 filedate 1981-04-25 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	% elepha.ax[s81,jmc]	Axioms for multiplication by addition in ELEPHANT
C00005 ENDMK
C⊗;
% elepha.ax[s81,jmc]	Axioms for multiplication by addition in ELEPHANT

% Our object is to prove

% ∀t.(P(t) ∧ start ≤ pc(t) ≤ start+5 ⊃ pc(t+1) = done ∨ P(t+1))
% ⊃ ∀t0.(pc(t0) = start ∧ P(t0) ⊃
% 		∃t2.(pc(t2) = done
% 			∧ p(t2) = m*n
% 			∧ ∀t1.(t0 ≤ t1 < t2 ⊃ P(t))))

% The induction is on the proposition

% Q(j) ≡ 

% 

declare INDVAR j t t0 t1 t2 m m0 m1 m2 n n0 n1 n2 start done ε NATNUM;
declare OPCONST i(NATNUM) = NATNUM, p(NATNUM) = NATNUM, pc(NATNUM) = NATNUM;

% Inductive assertions schema

declare PREDPAR P 1 alldone 1;

declare OPPAR rank(GENERAL) =NATNUM;

axiom floyd:
	∀t.(P(t) ∧ ¬alldone(t) ⊃ P(t+1) ∧ rank(t+1) < rank(t))
		⊃ ∀t0.(P(t0) ⊃ ∃t2.(t0≤t2 ∧ alldone(t2) ∧ P(t2)
			∧ ∀t1.(t0 ≤ t1 ∧ t1 < t2 ⊃ P(t1) ∧ ¬alldone(t1))))
;;

% fetch natnum.ax[s81,jmc];

axiom multprog:
∀t.(i(t+1) = IF pc(t) = start THEN n
ELSE IF pc(t) = start + 3 THEN i(t) - 1
ELSE IF start ≤ pc(t) ∧ pc(t) ≤ start + 5 THEN i(t)
ELSE i(t+1))

∀t.(p(t+1)  =IF pc(t) = start + 1 THEN 0
 ELSE IF pc(t) = start + 4 THEN p(t) + m
ELSE IF start ≤ pc(t) ∧ pc(t) ≤ start + 5 THEN p(t)
ELSE p(t+1))

∀t.(pc(t+1)  = IF pc(t) = start + 2 ∧ i(t) = 0 THEN done
ELSE IF pc(t) = start + 5 THEN start + 2
ELSE IF start ≤ pc(t) ∧ pc(t) ≤ start + 5 THEN pc(t) + 1
ELSE pc(t+1))
;;

axiom foo:
	∀j.(Q(j) ≡
	∀t.(rank(t) ≤ j ⊃ (P(t) ∧ ¬alldone(t) ⊃ P(t+1) ∧ rank(t+1) < rank(t))
		⊃ ∀t0.(P(t0) ⊃ ∃t2.(t0≤t2 ∧ alldone(t2) ∧ P(t2)
			∧ ∀t1.(t0 ≤ t1 ∧ t1 < t2 ⊃ P(t1) ∧ ¬alldone(t1))))))

% Make a non-Zoharian temporal operator R such that Rp means that p
% will be true the next time we return to the present level after "pushes"
% and "pops".